SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Logical framework</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Logical framework</span></span>

</h1>

</header>

<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><p>In <a href="Logic" title="Logic">logic</a>, a <b>logical framework</b> provides a means to define (or present) a logic as a signature in a higher-order <a href="Type_theory" title="Type theory">type theory</a> in such a way that <a href="Provability_logic" title="Provability logic">provability</a> of a formula in the original logic reduces to a <a href="Type_inhabitation" title="Type inhabitation">type inhabitation</a> problem in the framework type theory.<sup id="cite_ref-Jacobs2001_1-0" class="reference"><a href="#cite_note-Jacobs2001-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-Gabbay1994_2-0" class="reference"><a href="#cite_note-Gabbay1994-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> This approach has been used successfully for (interactive) <a href="Automated_theorem_proving" title="Automated theorem proving">automated theorem proving</a>. The first logical framework was <a href="Automath" title="Automath">Automath</a>; however, the name of the idea comes from the more widely known Edinburgh Logical Framework, <b>LF</b>. Several more recent proof tools like <a href="Isabelle_(theorem_prover)" class="mw-redirect" title="Isabelle (theorem prover)">Isabelle</a> are based on this idea.<sup id="cite_ref-Jacobs2001_1-1" class="reference"><a href="#cite_note-Jacobs2001-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.<sup id="cite_ref-BoveBarbosa2009_3-0" class="reference"><a href="#cite_note-BoveBarbosa2009-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Overview">Overview</h2></div>

<p>A logical framework is based on a general treatment of syntax, rules and proofs by means of a <a href="Dependent_type_theory" class="mw-redirect" title="Dependent type theory">dependently typed lambda calculus</a>. Syntax is treated in a style similar to, but more general than <a href="Per_Martin-L%C3%B6f" title="Per Martin-Löf">Per Martin-Löf</a>'s system of arities.

</p><p>To describe a logical framework, one must provide the following:

</p>

<ol><li>A characterization of the class of object-logics to be represented;</li>

<li>An appropriate meta-language;</li>

<li>A characterization of the mechanism by which object-logics are represented.</li></ol>

<p>This is summarized by:

</p>

<dl><dd>"<i>Framework = Language + Representation</i>."</dd></dl>

<p>In the case of the <b>LF logical framework</b>, the meta-language is the <a href="%CE%9B%CE%A0-calculus" class="mw-redirect" title="ΛΠ-calculus">λΠ-calculus</a>. This is a system of first-order dependent function types which are related by the <a href="Propositions_as_types_principle" class="mw-redirect" title="Propositions as types principle">propositions as types principle</a> to <a href="First-order_logic" title="First-order logic">first-order</a> <a href="Minimal_logic" title="Minimal logic">minimal logic</a>. The key features of the λΠ-calculus are that it consists of entities of three levels: objects, types and kinds (or type classes, or families of types). It is <a href="Impredicativity" title="Impredicativity">predicative</a>, all well-typed terms are <a href="Strongly_normalizing" class="mw-redirect" title="Strongly normalizing">strongly normalizing</a> and <a href="Church-Rosser" class="mw-redirect" title="Church-Rosser">Church-Rosser</a> and the property of being well-typed is <a href="Decidability_(logic)" title="Decidability (logic)">decidable</a>. However, <a href="Type_inference" title="Type inference">type inference</a> is undecidable.

</p><p>A logic is represented in the <b>LF logical framework</b> by the judgements-as-types representation mechanism. This is inspired by <a href="Per_Martin-L%C3%B6f" title="Per Martin-Löf">Per Martin-Löf</a>'s development of <a href="Immanuel_Kant" title="Immanuel Kant">Kant</a>'s notion of <a href="Judgement_(mathematical_logic)" class="mw-redirect" title="Judgement (mathematical logic)">judgement</a>, in the 1983 Siena Lectures. The two higher-order judgements, the hypothetical <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle J\vdash K}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle J\vdash K}</annotation>

</semantics>

</math></span><img src="./790acb3275cae6852dea98dece8c1afa460df68a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.248ex; height:2.176ex;" alt="{\displaystyle J\vdash K}" loading="lazy"></span> and the general, <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Lambda x\in J.K(x)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Lambda x\in J.K(x)}</annotation>

</semantics>

</math></span><img src="./c371a1816a4f3e19f1fb65b38e0c44bb4f9a0f07.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.494ex; height:2.843ex;" alt="{\displaystyle \Lambda x\in J.K(x)}" loading="lazy"></span>, correspond to the ordinary and dependent function space, respectively. The methodology of judgements-as-types is that judgements are represented as the types of their proofs. A <a href="Logical_system" class="mw-redirect" title="Logical system">logical system</a> <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {L}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {L}}}</annotation>

</semantics>

</math></span><img src="./9027196ecb178d598958555ea01c43157d83597c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.604ex; height:2.176ex;" alt="{\displaystyle {\mathcal {L}}}" loading="lazy"></span> is represented by its signature which assigns kinds and types to a finite set of constants that represents its syntax, its judgements and its rule schemes. An object-logic's rules and proofs are seen as primitive proofs of hypothetico-general judgements <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Lambda x\in C.J(x)\vdash K}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Lambda x\in C.J(x)\vdash K}</annotation>

</semantics>

</math></span><img src="./f2e3706f01af253abf28e1b5476662015a6d413a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.971ex; height:2.843ex;" alt="{\displaystyle \Lambda x\in C.J(x)\vdash K}" loading="lazy"></span>.

</p><p>An implementation of the LF logical framework is provided by the <a href="Twelf" title="Twelf">Twelf</a> system at <a href="Carnegie_Mellon_University" title="Carnegie Mellon University">Carnegie Mellon University</a>. Twelf includes

</p>

<ul><li>a logic programming engine</li>

<li>meta-theoretic reasoning about logic programs (termination, coverage, etc.)</li>

<li>an inductive <a href="Meta-logic" class="mw-redirect" title="Meta-logic">meta-logical</a> theorem prover</li></ul>

<ul><li><a href="Grammatical_Framework" class="mw-redirect" title="Grammatical Framework">Grammatical Framework</a></li>

<li><a href="Turnstile_(symbol)" title="Turnstile (symbol)">Turnstile (symbol)</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFBart_Jacobs2001" class="citation book cs1">Bart Jacobs (2001). <i>Categorical Logic and Type Theory</i>. Elsevier. p. 598. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-444-50853-9</bdi>.</cite></span>

</li>

<li id="cite_note-Gabbay1994-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-Gabbay1994_2-0">^</a></b></span> <span class="reference-text"><cite id="CITEREFDov_M._Gabbay1994" class="citation book cs1">Dov M. Gabbay, ed. (1994). <a rel="nofollow" class="external text" href="https://books.google.com/books?id=XqCu4XjHrIQC&pg=PA382"><i>What is a logical system?</i></a>. <a href="Clarendon_Press" class="mw-redirect" title="Clarendon Press">Clarendon Press</a>. p. 382. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-19-853859-2</bdi>.</cite></span>

</li>

<li id="cite_note-BoveBarbosa2009-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-BoveBarbosa2009_3-0">^</a></b></span> <span class="reference-text"><cite id="CITEREFAna_BoveLuis_Soares_BarbosaAlberto_Pardo2009" class="citation book cs1">Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). <a rel="nofollow" class="external text" href="https://books.google.com/books?id=YOqHiA5MYpEC&pg=PA48"><i>Language Engineering and Rigorous Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised, Selected Papers</i></a>. Springer. p. 48. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-642-03152-6</bdi>.</cite></span>

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2></div>

<ul><li><cite id="CITEREFFrank_Pfenning2002" class="citation book cs1"><a href="Frank_Pfenning" title="Frank Pfenning">Frank Pfenning</a> (2002). "Logical frameworks – a brief introduction". In <a href="Helmut_Schwichtenberg" title="Helmut Schwichtenberg">Helmut Schwichtenberg</a>, Ralf Steinbrüggen (ed.). <a rel="nofollow" class="external text" href="https://www.cs.cmu.edu/~fp/papers/mdorf01.pdf"><i>Proof and system-reliability</i></a> <span class="cs1-format">(PDF)</span>. <a href="Springer_Science%2BBusiness_Media" title="Springer Science+Business Media">Springer</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-4020-0608-1</bdi>.</cite></li>

<li><a href="Robert_Harper_(computer_scientist)" title="Robert Harper (computer scientist)">Robert Harper</a>, Furio Honsell and <a href="Gordon_Plotkin" title="Gordon Plotkin">Gordon Plotkin</a>. <i>A Framework For Defining Logics</i>. Journal of the Association for Computing Machinery, 40(1):143-184, 1993.</li>

<li><a href="Arnon_Avron" title="Arnon Avron">Arnon Avron</a>, Furio Honsell, Ian Mason and Randy Pollack. <i>Using typed lambda calculus to implement formal systems on a machine</i>. Journal of Automated Reasoning, 9:309-354, 1992.</li>

<li>Robert Harper. <i>An Equational Formulation of LF</i>. Technical Report, <a href="University_of_Edinburgh" title="University of Edinburgh">University of Edinburgh</a>, 1988. LFCS report ECS-LFCS-88-67.</li>

<li>Robert Harper, Donald Sannella and Andrzej Tarlecki. <i>Structured Theory Presentations and Logic Representations</i>. Annals of Pure and Applied Logic, 67(1-3):113-160, 1994.</li>

<li>Samin Ishtiaq and David Pym. <i>A Relevant Analysis of Natural Deduction</i>. Journal of Logic and Computation 8, 809-838, 1998.</li>

<li>Samin Ishtiaq and David Pym. <i>Kripke Resource Models of a Dependently-typed, Bunched <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lambda }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda }</annotation>

</semantics>

</math></span><img src="./b43d0ea3c9c025af1be9128e62a18fa74bedda2a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.355ex; height:2.176ex;" alt="{\displaystyle \lambda }" loading="lazy"></span>-calculus</i>. Journal of Logic and Computation 12(6), 1061-1104, 2002.</li>

<li>Per Martin-Löf. "<a rel="nofollow" class="external text" href="https://web.archive.org/web/20060104064335/http://www.hf.uio.no/filosofi/njpl/vol1no1/meaning/meaning.html">On the Meanings of the Logical Constants and the Justifications of the Logical Laws</a>." "Nordic Journal of Philosophical Logic", 1(1): 11-60, 1996.</li>

<li>Bengt Nordström, Kent Petersson, and Jan M. Smith. <i>Programming in Martin-Löf's Type Theory</i>. <a href="Oxford_University_Press" title="Oxford University Press">Oxford University Press</a>, 1990. (The book is out of print, but <a rel="nofollow" class="external text" href="http://www.cs.chalmers.se/Cs/Research/Logic/book/">a free version</a> has been made available.)</li>

<li>David Pym. <i>A Note on the Proof Theory of the <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lambda \Pi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda \Pi }</annotation>

</semantics>

</math></span><img src="./69f541a103ae7d83ab6ab2a9a18565586c4b52ce.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.098ex; height:2.176ex;" alt="{\displaystyle \lambda \Pi }" loading="lazy"></span>-calculus</i>. Studia Logica 54: 199-230, 1995.</li>

<li>David Pym and <a href="Lincoln_Wallen" title="Lincoln Wallen">Lincoln Wallen</a>. <i>Proof-search in the <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lambda \Pi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda \Pi }</annotation>

</semantics>

<li>Didier Galmiche and David Pym. <i>Proof-search in type-theoretic languages:an introduction</i>. Theoretical Computer Science 232 (2000) 5-53.</li>

<li>Philippa Gardner. <i>Representing Logics in Type Theory</i>. Technical Report, University of Edinburgh, 1992. LFCS report ECS-LFCS-92-227.</li>

<li>Gilles Dowek. <i>The undecidability of typability in the lambda-pi-calculus</i>. In M. Bezem, J.F. Groote (Eds.), Typed Lambda Calculi and Applications. Volume 664 of <i>Lecture Notes in Computer Science</i>, 139-145, 1993.</li>

<li>David Pym. <i>Proofs, Search and Computation in General Logic</i>. Ph.D. thesis, University of Edinburgh, 1990.</li>

<li>David Pym. <i>A Unification Algorithm for the <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lambda \Pi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda \Pi }</annotation>

</semantics>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><a rel="nofollow" class="external text" href="https://www.cs.cmu.edu/~fp/lfs-impl.html">Specific Logical Frameworks and Implementations</a> (a list maintained by <a href="Frank_Pfenning" title="Frank Pfenning">Frank Pfenning</a>, but mostly dead links from 1997)</li></ul></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2023-11-04" href="https://en.wikipedia.org/wiki/?title=Logical_framework&oldid=1183530085">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>